\begin{tabbing}
when{-}after($e$;${\it info}$;${\it pred?}$;${\it init}$;${\it Trans}$;${\it val}$;${\it time}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if first($e$)\+
\\[0ex]then let $s$ = $\lambda$$x$.${\it init}$(loc($e$),$x$)+${\it time}$($e$) in $<$$s$, ${\it Trans}$(loc($e$),kind($e$),${\it val}$($e$),$s$)$>$
\\[0ex]else let $s$ = \=when{-}after(pred($e$);${\it info}$;${\it pred?}$;${\it init}$;${\it Trans}$;${\it val}$;${\it time}$).2\+
\\[0ex]+(${\it time}$($e$)) {-} (${\it time}$(pred($e$))) in $<$$s$, ${\it Trans}$(loc($e$),kind($e$),${\it val}$($e$),$s$)$>$
\-\\[0ex]fi 
\\[0ex]
\-\\[0ex]{\em clarification:}
\\[0ex]
\\[0ex]when{-}after($e$;${\it info}$;${\it pred?}$;${\it init}$;${\it Trans}$;${\it val}$;${\it time}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if first(${\it pred?}$;$e$)\+
\\[0ex]then let $s$\= = $\lambda$$x$.${\it init}$(loc(${\it info}$;$e$),$x$)+${\it time}$($e$) in\+
\\[0ex]$<$$s$, ${\it Trans}$(loc(${\it info}$;$e$),kind(${\it info}$;$e$),${\it val}$($e$),$s$)$>$
\-\\[0ex]else let $s$\= = \=when{-}after(pred(${\it pred?}$;$e$);${\it info}$;${\it pred?}$;${\it init}$;${\it Trans}$;${\it val}$;${\it time}$).2\+\+
\\[0ex]+(${\it time}$($e$)) {-} (${\it time}$(pred(${\it pred?}$;$e$))) in
\-\\[0ex]$<$$s$, ${\it Trans}$(loc(${\it info}$;$e$),kind(${\it info}$;$e$),${\it val}$($e$),$s$)$>$
\-\\[0ex]fi 
\-\\[0ex]\emph{(recursive)}
\end{tabbing}